Robbins algebra

In abstract algebra, a Robbins algebra is an algebra containing a single binary operation, usually denoted by \lor, and a single unary operation usually denoted by \neg. These operations satisfy the following axioms:

For all elements a, b, and c:

  1. Associativity: a \lor \left(b \lor c\right) = \left(a \lor b\right) \lor c
  2. Commutativity: a \lor b = b \lor a
  3. Robbins's axiom: \neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = a

History

In 1933, Edward Huntington proposed a new set of axioms for Boolean algebras, consisting of (1) and (2) above, plus:

From these axioms, Huntington derived the usual axioms of Boolean algebra. Specifically, what Huntington proved was that if we take \lor to interpret Boolean join, \neg to interpret Boolean complement and use \lor and \neg to define Boolean meet and the constants 0 and 1, then the axioms for a Boolean algebra are satisfied.

Very soon thereafter, Herbert Robbins posed the Robbins conjecture (also called the Robbins problem), namely that the Huntington axiom could be replaced with Robbins's axiom, and the result would still be a Boolean algebra in the sense explained in the previous paragraph. Pending verification of the conjecture, the system of Robbins was called a "Robbins algebra."

Verifying the Robbins conjecture required proving Huntington's axiom, or some other axiomatization of a Boolean algebra, as theorems of a Robbins algebra. Huntington, Robbins, Alfred Tarski, and others worked on the problem, but failed to find a proof or counterexample.

William McCune proved the conjecture in 1996, using the automated theorem prover EQP. For a complete proof of the Robbins conjecture in one consistent notation and following McCune closely, see Mann (2003). Dahn (1998) simplified McCune's machine proof.

References